Theory Case_Labeling.Case_Labeling

theory Case_Labeling
imports Main
keywords "print_nested_cases" :: diag
begin

section ‹Labeling Subgoals›

context begin
  qualified type_synonym prg_ctxt_var = unit
  qualified type_synonym prg_ctxt = "string × nat × prg_ctxt_var list"

  text ‹Embed variables in terms›
  qualified definition VAR :: "'v ⇒ prg_ctxt_var" where
    "VAR _ = ()"

  text ‹Labeling of a subgoal›
  qualified definition VC :: "prg_ctxt list ⇒ 'a ⇒ 'a" where
    "VC ct P ≡ P"

  text ‹Computing the statement numbers and context›
  qualified definition CTXT :: "nat ⇒ prg_ctxt list ⇒ nat ⇒ 'a ⇒ 'a" where
    "CTXT inp ct outp P ≡ P"

  text ‹Labeling of a term binding or assumption›
  qualified definition BIND :: "string ⇒ nat ⇒ 'a ⇒ 'a" where
    "BIND name inp P ≡ P"

  text ‹Hierarchy labeling›
  qualified definition HIER :: "prg_ctxt list ⇒ 'a ⇒ 'a" where
    "HIER ct P ≡ P"

  text ‹Split Labeling. This is used as an assumption›
  qualified definition SPLIT :: "'a ⇒ 'a ⇒ bool" where
    "SPLIT v w ≡ v = w"

  text ‹Disambiguation Labeling. This is used as an assumption›
  qualified definition DISAMBIG :: "nat ⇒ bool" where
    "DISAMBIG n ≡ True"

  lemmas LABEL_simps = BIND_def CTXT_def HIER_def SPLIT_def VC_def

  lemma Initial_Label: "CTXT 0 [] outp P ⟹ P"
    by (simp add: Case_Labeling.CTXT_def)

  lemma
    BIND_I: "P ⟹ BIND name inp P" and
    BIND_D: "BIND name inp P ⟹ P" and
    VC_I: "P ⟹ VC ct P"
    unfolding Case_Labeling.BIND_def Case_Labeling.VC_def .

  lemma DISAMBIG_I: "(DISAMBIG n ⟹ P) ⟹ P"
    by (auto simp: DISAMBIG_def Case_Labeling.VC_def)

  lemma DISAMBIG_E: "(DISAMBIG n ⟹ P) ⟹ P"
    by (auto simp: DISAMBIG_def)

  text ‹Lemmas for the tuple postprocessing›
  lemma SPLIT_reflection: "SPLIT x y ⟹ (x ≡ y)"
    unfolding SPLIT_def by (rule eq_reflection)

  lemma rev_SPLIT_reflection: "(x ≡ y) ⟹ SPLIT x y"
    unfolding SPLIT_def ..

  lemma SPLIT_sym: "SPLIT x y ⟹ SPLIT y x"
    unfolding SPLIT_def by (rule sym)

  lemma SPLIT_thin_refl: "⟦SPLIT x x; PROP W⟧ ⟹ PROP W" .

  lemma SPLIT_subst: "⟦SPLIT x y; P x⟧ ⟹ P y"
    unfolding SPLIT_def by hypsubst

  lemma SPLIT_prodE:
    assumes "SPLIT (x1, y1) (x2, y2)"
    obtains "SPLIT x1 x2" "SPLIT y1 y2"
    using assms unfolding SPLIT_def by auto


end

text ‹
  The labeling constants were qualified to not interfere with any other theory.
  The following locale allows using a nice syntax in other theories
›

locale Labeling_Syntax begin
  abbreviation VAR where "VAR ≡ Case_Labeling.VAR"
  abbreviation VC (‹V⟨(2_,_:/ _)⟩›) where "VC bl ct  ≡ Case_Labeling.VC (bl # ct)"
  abbreviation CTXT (‹C⟨(2_,_,_:/ _⟩)›) where "CTXT ≡ Case_Labeling.CTXT"
  abbreviation BIND (‹B⟨(2_,_:/ _⟩)›) where "BIND ≡ Case_Labeling.BIND"
  abbreviation HIER (‹H⟨(2_:/ _⟩)›) where "HIER ≡ Case_Labeling.HIER"
  abbreviation SPLIT where "SPLIT ≡ Case_Labeling.SPLIT"
end

text ‹Lemmas for converting terms from @{term Suc}/@{term "0::nat"} notation to numerals›
lemma Suc_numerals_conv:
  "Suc 0 = Numeral1"
  "Suc (numeral n) = numeral (n + num.One)"
  by auto

lemmas Suc_numeral_simps = Suc_numerals_conv add_num_simps


section ‹Casify›

text ‹
  Introduces a command @{command print_nested_cases}. This is similar to @{command print_cases},
  but shows also the nested cases.
›
ML_file ‹print_nested_cases.ML›

ML_file ‹util.ML›

text ‹Introduces the proof method.›
ML_file ‹casify.ML›


ML ‹
  val casify_defs = Casify.Options { simp_all_cases=true, split_right_only=true, protect_subgoals=false }
›

method_setup prepare_labels = ‹
  Scan.succeed (fn ctxt => SIMPLE_METHOD (ALLGOALS (Casify.prepare_labels_tac ctxt)))
› "VCG labelling: prepare labels"

method_setup casify = ‹Casify.casify_method_setup casify_defs›
  "VCG labelling: Turn the labels into cases"

end