Theory Codatatype_Witnesses

theory Codatatype_Witnesses
imports BNF_Nonuniform_Fixpoint BNF_Axiomatization
theory Codatatype_Witnesses
  imports
    "../code/BNF_Nonuniform_Fixpoint" 
    "~~/src/HOL/Library/BNF_Axiomatization"
begin
declare [[bnf_internals,typedef_overloaded]]

bnf_axiomatization ('a0,'a1,'T0,'T1) GG
  [wits: "'a0 ⇒ 'T1 ⇒ ('a0,'a1,'T0,'T1) GG" 
    "'a1 ⇒ 'T0 ⇒ ('a0,'a1,'T0,'T1) GG"
    (* breaks perfectness, but is better for illustration: *)
    "'a0 ⇒ 'a1 ⇒ 'T0 ⇒ 'T1 ⇒ ('a0,'a1,'T0,'T1) GG"
    ]
bnf_axiomatization ('a0,'a1) FF1_1 
  [wits: "'a0 ⇒ ('a0,'a1) FF1_1" "'a1 ⇒ ('a0,'a1) FF1_1"]
bnf_axiomatization ('a0,'a1) FF1_2
  [wits: "'a0 ⇒ 'a1 ⇒ ('a0,'a1) FF1_2"]
bnf_axiomatization ('a0,'a1) FF2_1 
  [wits: "'a0 ⇒ ('a0,'a1) FF2_1"]
bnf_axiomatization ('a0,'a1) FF2_2 
  [wits: "'a0 ⇒ ('a0,'a1) FF2_2"]

nonuniform_codatatype
  ('a0, 'a1) T = C "('a0, 'a1, (('a0, 'a1) FF1_1, ('a0, 'a1) FF1_2) T, (('a0, 'a1) FF2_1, ('a0, 'a1) FF2_2) T) GG"

type_synonym depth = "label_T list"

  (* Labels: *)
abbreviation "L1 ≡ T.L_2_T"
abbreviation "L2 ≡ T.L_1_T"


  (* DEEP EMBEDDEDING OF THE WITNESS INFRASTRUCTURE *)

  (* This deep embedding is only used for guiding the choices in 
  witness proof, but is not actually used in the proof. It can be done in ML. *)

  (* witness positions for the Fs: *)
datatype witposFs = A0 | A1 
  (* witness positions for G: *)
datatype witposG = AA0 | AA1 | T0 | T1 
  
  (* The numbers of witnesses for each BNF involved: *)
definition "nwitsG ≡ 3"
definition "nwitsF1_1 ≡ 2"  definition "nwitsF1_2 ≡ 1" 
definition "nwitsF2_1 ≡ 1"  definition "nwitsF2_2 ≡ 1" 

declare numeral_2_eq_2[simp]

lemmas nwits_defs = nwitsG_def 
  nwitsF1_1_def nwitsF1_2_def 
  nwitsF2_1_def nwitsF2_2_def

  (* ... and the set of witness positions for each witness: *)
fun wp_G where
  "wp_G 0 = {AA0,T1}"
| "wp_G (Suc 0) = {AA1,T0}"
| "wp_G (Suc (Suc 0)) = {AA0,AA1,T0,T1}"
  
fun wp_F1_1 where
  "wp_F1_1 0 = {A0}"
| "wp_F1_1 (Suc 0) = {A1}"
fun wp_F1_2 where
  "wp_F1_2 (0 :: nat) = {A0,A1}" 
  (****) 
fun wp_F2_1 where "wp_F2_1 (0 :: nat) = {A0}" 
fun wp_F2_2 where "wp_F2_2 (0 :: nat) = {A0}"

fun trans :: "witposFs set ⇒ label_T × nat × nat × nat ⇒ 
  witposFs set ⇒ bool" 
  where 
    "trans S (L1,i,i_1,i_2) S' ⟷ 
    i < nwitsG ∧ i_1 < nwitsF1_1 ∧ i_2 < nwitsF1_2 ∧
    (AA0 ∈ wp_G i ⟶ A0 ∈ S) ∧ 
    (AA1 ∈ wp_G i ⟶ A1 ∈ S) ∧ 
    S' = {x . x = A0 ∧ wp_F1_1 i_1 ⊆ S} ∪ 
    {x . x = A1 ∧ wp_F1_2 i_2 ⊆ S}"
  |"trans S (L2,i,i_1,i_2) S' ⟷ 
    i < nwitsG ∧ i_1 < nwitsF2_1 ∧ i_2 < nwitsF2_2 ∧ 
    (AA0 ∈ wp_G i ⟶ A0 ∈ S) ∧ 
    (AA1 ∈ wp_G i ⟶ A1 ∈ S) ∧ 
    S' = {x . x = A0 ∧ wp_F2_1 i_1 ⊆ S} ∪ 
    {x . x = A1 ∧ wp_F2_2 i_2 ⊆ S}"
  
  
    (* INFRASTRUCTURE FOR GUIDING THE PROOF THAT {A1} IS A WITNESS FOR T *)
  
definition "S1 ≡ {A1}" (* S1 is the to-be-proved set of witness positions *) 
definition "S0 ≡ {A0}" 
definition "S01 ≡ {A0,A1}"  
lemmas S_defs = S1_def S0_def S01_def 

  (* Semantically, each Sx encodes a witnessing situation, for the current depth u,
  for "('a0,'a1) shape_1_T" and "('a0,'a1) shape_1_T". Namely, Sx contains Ai 
  just in case shape_i_T has a witness of depth u. *)

  (* The transition relation trans (which is btw. independent of the to-be-proved 
  set of witnesses, encodes possibilities for moving between "u" (represented by a set 
  S) and an element g :: (('a0,'a1) shape_1_T, ('a0,'a1)shape_2_T, depth, depth) G 
  of a raw_T-coalgebra over depths. The labels on the 
  transition show how "g" can be constructed using the witnesses of 
  G, F1_1, F1_2, F2_1, F2_2. Namely: 
  -- S provides (by its semantics), elements of ('a0,'a1) shape_1_T and/or 
  ('a0,'a1)shape_2_T
  -- We need to pick a witness witi_G for G that covers what S provides 
  on the first 2 positions
  -- We look at the remaining two positions (the recursive ones) and at which 
  of them witi_G requires a witness. E.g., say both recursive positions need witnesses;
  then we need to have two transitions (with the same i!) "trans S (L1,i,_,_) S1" 
  and "trans S (L2,i,_,_) S0", leading to states S1 and S0 encoding "L1 # u" 
  and "L2 # u".   
  -- The remaining slots on the labels are filled with choices of witnesses 
  leading to these new states S1 and S0:
  ----- "trans S (L1,i,i1,i2) S1" means we pick wit_i1_F1_1 and wit_i2_F1_2
  ----- "trans S (L2,i,i1,i2) S0" means we pick wit_i1_F2_1 and wit_i2_F2_2
  *)

  (* So we need to search (in ML) for finite sets {S1,...Sk}, such that:
  -- S1 contains the initial configuration, here, {A0}
  -- For each Sx, there exists i < nwitsG such that: 
  ---- if T0 ∈ wp_G i, then there exist Sy, i1 < nwitsF1_1, i2 < nwitsF1_2 
  and a transition "trans Sx (L1,i,i1,i2) Sy"
  ---- if T1 ∈ wp_G i, then there exist Sy, i1 < nwitsF1_1, i2 < nwitsF1_2 
  and a transition "trans Sx (L2,i,i1,i2) Sy"
  
  An example follows:
  *)

lemma
  "trans S1 (L1,1,1,0) S0"
  "trans S0 (L2,0,0,0) S01"
  "trans S01 (L1,2,0,0) S01"
  "trans S01 (L2,1,0,0) S01"
  by (auto simp: nwits_defs S_defs)

    (* THE WITNESS PROOF: *)

    (* Inductive definition of depths matching the transitions between "S"s:  *)
inductive
  is_S1 :: "depth ⇒ bool" and
  is_S0 :: "depth ⇒ bool" and
  is_S01 :: "depth ⇒ bool" 
  where 
    "is_S1 []"
  | "is_S1 u ⟹ is_S0 (L1 # u)"
  | "is_S0 u ⟹ is_S01 (L2 # u)"
  | "is_S01 u ⟹ is_S01 (L1 # u)"
  | "is_S01 u ⟹ is_S01 (L2 # u)"

definition "is_S u = (is_S1 u ∨ is_S0 u ∨ is_S01 u)"

lemmas is_S_Nil = is_S_def[of "[]", unfolded is_S1.simps simp_thms]
  
context
  fixes dummy :: "'a0 × 'a1"
    and a1 :: 'a1
begin

definition pred1 :: "depth ⇒ ('a0, 'a1) shape_1_T ⇒ bool" where
  "pred1 u sh1 = (T.invar_shape_1_T u sh1 ∧ pred_shape_1_T (λ_. False) (λx. x = a1) sh1)"
definition pred2 :: "depth ⇒ ('a0, 'a1) shape_2_T ⇒ bool" where
  "pred2 u sh2 = (T.invar_shape_2_T u sh2 ∧ pred_shape_2_T (λ_. False) (λx. x = a1) sh2)"

abbreviation "spred u g ≡
  pred_pre_T (pred1 u) (pred2 u) (λu'. u' = L2 # u ∧ is_S u') (λu'. u' = L1 # u ∧ is_S u') g"

definition "wcoalg u = Eps (spred u)"

primcorec wit :: "depth ⇒ ('a0,'a1) raw_T" where 
  "wit u = T.raw_T.Ctor_T (map_pre_T id id wit wit (wcoalg u))"
  
  (*
  The statement pred_Si, entirely determined by Si, makes explicit 
  what Si encodes, namely, the existence of witnesses for the given depth. *)

  (* The only inductive proof needed -- shows that if depths follow 
  the transitions encoded in the deep embedding, they achieve what 
  their corresponding sets of states encode. *)

lemma is_pred_S:
  "(is_S1 u ⟶(∃sh2::('a0,'a1) shape_2_T. pred2 u sh2)) ∧ 
   (is_S0 u ⟶ (∃sh1::('a0,'a1) shape_1_T. pred1 u sh1)) ∧
  (is_S01 u ⟶ (∃sh1::('a0,'a1) shape_1_T. pred1 u sh1) ∧ (∃sh2::('a0,'a1) shape_2_T. pred2 u sh2))"
  apply (rule is_S1_is_S0_is_S01.induct; unfold pred1_def[abs_def] pred2_def[abs_def];
      ((erule exE conjE)+)?; (rule conjI)?)
         apply (rule
             exI[of _ "T.shape_1_T.leaf_T _"]
             exI[of _ "T.shape_2_T.leaf_T _"]
             exI[of _ "T.shape_1_T.node_1_T (arg.wit1_pre_T_1_0 _)"]
             exI[of _ "T.shape_1_T.node_1_T (arg.wit2_pre_T_1_0 _)"]
             exI[of _ "T.shape_2_T.node_1_T (arg.wit_pre_T_1_1 _ _)"]
             exI[of _ "T.shape_1_T.node_0_T (arg.wit_pre_T_0_0 _)"]
             exI[of _ "T.shape_2_T.node_0_T (arg.wit_pre_T_0_1 _)"],
          ((hypsubst | assumption | drule
          arg.arg.pre_T_0_0.wit
          arg.arg.pre_T_0_1.wit
          arg.arg.pre_T_1_0.wit1
          arg.arg.pre_T_1_0.wit2
          arg.arg.pre_T_1_1.wit | (rule conjI ballI)+ | simp only:
          list.case simp_thms if_True if_False label_T.distinct
          T.invar_shape_1_T.simps T.invar_shape_2_T.simps
          shape_1_T.pred_inject shape_2_T.pred_inject
          arg.arg.pre_T_0_0.pred_set
          arg.arg.pre_T_0_1.pred_set
          arg.arg.pre_T_1_0.pred_set
          arg.arg.pre_T_1_1.pred_set)+; fail) [])+
  done

lemmas is_pred_S1 = is_pred_S[THEN conjunct1, rule_format]
lemmas is_pred_S0 = is_pred_S[THEN conjunct2, THEN conjunct1, rule_format]
lemmas is_pred_S01 = is_pred_S[THEN conjunct2, THEN conjunct2, rule_format]

  (* Now we reify the coalgebra transitions encoded by the deep embedding: *)
lemma is_S_closed:
  "is_S u ⟹ spred u (wcoalg u)"
  unfolding is_S_def wcoalg_def
  apply (rule someI_ex)
  apply (elim disjE; frule is_pred_S1 is_pred_S0 is_pred_S01; unfold pre_T.pred_set; (erule conjE exE)+)
    apply (rule exI[of _ "wit1_pre_T _ _"] exI[of _ "wit2_pre_T _ _"] exI[of _ "wit3_pre_T _ _"],
      ((hypsubst | assumption | drule pre_T.wit1 pre_T.wit2 pre_T.wit3 | rule conjI ballI |
          simp only: is_S1_is_S0_is_S01.intros list.simps simp_thms)+; fail))+
  done
  
  (* Everything else follows from the properties we proved about the 
  states and transitions of the coalgebra. *)
  
lemma pred_raw_T_wit: "is_S u ⟹ pred_raw_T (λ_. False) (λx. x = a1) (wit u)"
  apply (rule raw_T.rel_coinduct[THEN iffD2[OF raw_T.pred_rel],
    of "eq_onp (λx. ∃u. x = wit u ∧ is_S u)"])
   apply (unfold eq_onp_def simp_thms)
   apply (rule exI conjI refl)+
   apply assumption
  apply (erule thin_rl)
  apply (erule exE conjE)+
  apply hypsubst_thin
  apply (drule is_S_closed)
  apply (unfold pre_T.pred_rel shape_1_T.pred_rel shape_2_T.pred_rel wit.sel pre_T.rel_map
    id_apply eq_onp_def pred1_def pred2_def)
  apply (erule pre_T.rel_mono_strong)
     apply (erule conjE)+
     apply hypsubst_thin
     apply (erule shape_1_T.rel_mono_strong; (erule conjunct1 | assumption))
    apply (erule conjE)+
    apply hypsubst_thin
    apply (erule shape_2_T.rel_mono_strong; (erule conjunct1 | assumption))
   apply (erule exE conjE)+
   apply hypsubst_thin
   apply ((rule exI conjI refl | assumption)+) []
  apply (erule exE conjE)+
  apply hypsubst_thin
  apply ((rule exI conjI refl | assumption)+) []
  done

lemma invar_wit: "is_S u ⟹ T.invar_raw_T u (wit u)"
  apply (rule invar_raw_T.coinduct[of "λu' w. ∃u. u' = u ∧ w = wit u ∧ is_S u"])
   apply (rule exI conjI refl)+
   apply assumption
  apply (erule thin_rl)
  apply (erule exE conjE)+
  apply hypsubst_thin
  apply (rule exI conjI refl)+
   apply (rule wit.ctr)
  apply (drule is_S_closed)
  apply (unfold pre_T.pred_map)
  apply (erule pre_T.pred_mono_strong)
     apply (unfold id_apply o_apply pred1_def)
     apply (erule conjunct1)
    apply (unfold id_apply o_apply pred2_def)
    apply (erule conjunct1)
   apply (erule conjE)
   apply hypsubst_thin
   apply (rule disjI1)
   apply (rule exI conjI refl)+
   apply assumption
  apply (erule conjE)
  apply hypsubst_thin
  apply (rule disjI1)
  apply (rule exI conjI refl)+
  apply assumption
  done

lemmas invar_wit_Nil = invar_wit[OF is_S_Nil]
lemmas T_wit_Nil =
  pred_raw_T_wit[OF is_S_Nil, unfolded raw_T.pred_set, THEN conjunct1, THEN bspec]
  pred_raw_T_wit[OF is_S_Nil, unfolded raw_T.pred_set, THEN conjunct2, THEN bspec]

end

end